FDL - Step of Proof: fseg_extend

Step of Proof: fseg_extend

Inference at *
Iof proof for Lemma fseg extend:

T:Type, l1:(T List), v:T, l2:(T List).

fseg(T;l1;l2)

((||l1|| < ||l2||) c

(l2[(||l2|| - (||l1||+1))] = v))

fseg(T;[v / l1];l2)

by ((((((((Unfold `fseg` 0)

CollapseTHEN (Auto'))

)

CollapseTHEN (D (-1)

))

)

CollapseTHEN (

CExRepD

))

)

CollapseTHEN (((WeakSubstFor l2 0)

CollapseTHEN ((((Assert

(

null(L)))

THENL [(

T((((((DVar `L')

CollapseTHEN (Reduce 0))

)

CollapseTHEN (Auto

))

)

CollapseTHEN (((((

C((if (first_bool T:b) then HypSubst' else RevHypSubst') ( -3)( -2))

)
THENM (Reduce (-2)))

)

THECollapseTHEN (Auto

))

))

); Id]

)
TCollapseTHEN (((InstLemma `last_lemma` [T;L])

TCoCollapseTHENA (Auto

))

))

))

))

TC1:

TC1: 1. T : Type
TC1: 2. l1 : T List
TC1: 3. v : T
TC1: 4. l2 : T List
TC1: 5. L : T List
TC1: 6. l2 = (L @ l1)
TC1: 7. ||l1|| < ||l2||
TC1: 8. l2[(||l2|| - (||l1||+1))] = v
TC1: 9.

(

null(L))
TC1: 10.

L':T List. (L = (L' @ [last(L)]))
TC1:

L@0:T List. ((L @ l1) = (L@0 @ [v / l1]))
TC.

Definitions A, b, null(as), fseg(T;L1;L2), A c B, A List, i j , A B, P Q, P Q, P & Q, [car / cdr], SQType(T), {T}, s ~ t, Top, x:A.B(x), l[i], n - m, n+m, #$n, as @ bs, [], , t T, S T, |g|, , , {x:A| B(x)} , a < b, s = t, type List, Type, False, Void, True, ||as||, x:A. B(x), P Q, x:AB(x), x:A. B(x), x:A B(x)

Lemmas select wf, append wf, not wf, false wf, non neg length, cons one one, guard wf, nat wf, length wf nat, top wf, length wf1, member wf, true wf, last lemma